package gov.nasa.jpf.symbc.numeric;

import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Queue;
import java.util.Set;

public class DependencyCalc {

	public static PathCondition calcMinPC(PathCondition pc) {
		// calculate the minimal constraints
		Set<Constraint> minConstraints = calcMinConstraints(pc);

		PathCondition minPC = new PathCondition();
		minPC.header = copyConstraint(pc.header);
		Constraint c = minPC.header;
		for (Constraint d = pc.header.and; d != null; d = d.getTail()) {
			if (minConstraints.contains(d)) {
				c.and = copyConstraint(d);
				c = c.and;
			}
		}
		minPC.recomputeCount();
		minPC.resetHashCode();
		
		return minPC;
	}
	
	/**
	 * Calculate the subset of constraints in the path condition that depend
	 * (directly or indirectly) on the "fresh" constraint of the given path
	 * condition.
	 * 
	 * @param pc
	 *            the path condition
	 * @return the set of dependent constraints
	 */
	public static Set<Constraint> calcMinConstraints(PathCondition pc) {
		assert pc.header != null;
		Map<Constraint, Set<Integer>> constraintVars = new HashMap<Constraint, Set<Integer>>();
		Map<Integer, Set<Constraint>> varConstraints = new HashMap<Integer, Set<Constraint>>();
		//pc.setUniqueVarsCount(varConstraints.size());
		for (Constraint c = pc.header; c != null; c = c.getTail()) {
			c.accept(new VarCollectionVisitor(c, constraintVars, varConstraints));
		}
		Set<Constraint> minConstraints = new HashSet<Constraint>();
		Queue<Constraint> workset = new LinkedList<Constraint>();
		workset.add(pc.header);
		minConstraints.add(pc.header);
		while (!workset.isEmpty()) {
			Constraint c = workset.remove();
			for (Integer v : constraintVars.get(c)) {
				for (Constraint d : varConstraints.get(v)) {
					if (!minConstraints.contains(d)) {
						workset.add(d);
						minConstraints.add(d);
					}
				}
			}
		}
		return minConstraints;
	}
	
	public static Constraint copyConstraint(Constraint cRef) {

		if (cRef instanceof LinearIntegerConstraint)
			return new LinearIntegerConstraint((LinearIntegerConstraint) cRef);
		else if (cRef instanceof NonLinearIntegerConstraint)
			return new NonLinearIntegerConstraint(
					(NonLinearIntegerConstraint) cRef);
		else if (cRef instanceof RealConstraint)
			return new RealConstraint((RealConstraint) cRef);
		else if (cRef instanceof MixedConstraint)
			return new MixedConstraint((MixedConstraint) cRef);
		else {
			System.out
					.println("Should never happen, missed a type in copyConstraint");
			return null;
		}
	}

	public static int countUniqueVars(PathCondition pc) {
		Map<Constraint, Set<Integer>> constraintVars = new HashMap<Constraint, Set<Integer>>();
		Map<Integer, Set<Constraint>> varConstraints = new HashMap<Integer, Set<Constraint>>();
		for (Constraint c = pc.header; c != null; c = c.getTail()) {
			c.accept(new VarCollectionVisitor(c, constraintVars, varConstraints));
		}
		return varConstraints.size();
	}

	/**
	 * A visitor that collects all variables that appear in a constraint and
	 * updates a mapping from constraints to set of variables and a second
	 * mapping from variables to set of constraints.
	 */
	private final static class VarCollectionVisitor extends
			ConstraintExpressionVisitor {

		/**
		 * The constraint that this visitor is exploring.
		 */
		private Constraint constraint;

		/**
		 * The constraint-to-variables map to update.
		 */
		private Map<Constraint, Set<Integer>> constraintToVars;

		/**
		 * The variable-to-constraints map to update.
		 */
		private Map<Integer, Set<Constraint>> varToConstraints;

		/**
		 * Constructor for the visitor.
		 * 
		 * @param constraint
		 *            the constraint being traversed
		 * @param constraintToVars
		 *            the constraint-to-variables map
		 * @param varToConstraints
		 *            the variable-to-constraints map
		 */
		public VarCollectionVisitor(Constraint constraint,
				Map<Constraint, Set<Integer>> constraintToVars,
				Map<Integer, Set<Constraint>> varToConstraints) {
			this.constraint = constraint;
			this.constraintToVars = constraintToVars;
			this.varToConstraints = varToConstraints;
		}

		/**
		 * Update the two mappings to reflect that a variable appears in the
		 * constraint being traversed. This means that the variable is added to
		 * the set of variables that the current constraint maps to, and that
		 * the current constraint is added to the variable's set of constraints.
		 * 
		 * @param v
		 */
		private void addVariable(int v) {
			// add mapping c -> v
			Set<Integer> vs = constraintToVars.get(constraint);
			if (vs == null) {
				vs = new HashSet<Integer>();
			}
			vs.add(v);
			constraintToVars.put(constraint, vs);
			// add mapping v -> c
			Set<Constraint> cs = varToConstraints.get(v);
			if (cs == null) {
				cs = new HashSet<Constraint>();
			}
			cs.add(constraint);
			varToConstraints.put(v, cs);
		}

		@Override
		public void postVisit(SymbolicInteger node) {
			addVariable(node.hashCode());
		}

		@Override
		public void postVisit(SymbolicReal node) {
			addVariable(node.hashCode());
		}

	}

	
}
